The present invention is related to computer-aided design (CAD), and more particularly to property coverage in formal verification of integrated circuits.
One of the problems with modem logic design is the verification that the design actually works in the way it was intended to work. Undetected errors in the logic design may cause costly redesigns, or even loss of consumer confidence in the product if the product has been released on the market.
Model checking is one method of verifying designs. Model checking is a formal verification (FV) technology for property verification. A property specifies the desired values of particular circuit signals at various points in time in relation to other signals. Given a model of a design and some desired properties, a model checker like Symbolic Model Verifier (SMV) verifies whether the model satisfies all the desired properties under all possible input sequences. The properties are specified in a property specification language such as Computation Tree Logic (CTL). Although model checking is an exhaustive FV technique, a bug can escape the model checking effort if the properties specified by the user do not check for the erroneous behavior caused by the bug. Such erroneous behavior usually occurs in some obscure corner case that has been missed by the user. This is quite common when the specification has to be manually decomposed into a set of smaller, more tractable properties that are verifiable by the model checker. To reduce bug escapes, the user needs to continuously strengthen existing properties and specify new properties, without knowing if the additional verification is insufficient or redundant.
Logic simulation is another method of verifying designs. In existing simulation-based verification methodologies, coverage metrics are used to improve the quality of a test suite and estimate the progress of the verification task. For example, a common coverage metric for simulation is xe2x80x9ccode coveragexe2x80x9d, which measures the fraction of hardware description language (xe2x80x9cHDLxe2x80x9d) statements exercised during simulation. An xe2x80x9cobservability based code coveragexe2x80x9d enhances this metric by factoring potential error propagation to observability points. xe2x80x9cTransition coveragexe2x80x9d is another metric for control state machines. Such coverage metrics are effective in reducing bug escapes by pointing out coverage holes in the test suite.
However, the existing coverage metrics for simulation do not apply directly to model checking, e.g., a naive interpretation of the code coverage or transition coverage metric on a model checking task gives a meaningless coverage of 100% for every property. Logic simulation is dynamic and its coverage is driven by input simulation vectors, whereas model checking is static without any notion of circuit execution. Unlike logic simulation, the likelihood of having a bug escape detection in a model checking effort depends solely on the quality of the properties verified. Therefore, what is needed is a coverage metric that estimates the xe2x80x9ccompletenessxe2x80x9d (i.e. the quality) of a set of properties against which the design has been verified.
For example, consider the CTL formula for count, a modulo-5 counter, with stall and reset as external inputs:
AG[((-stallxcex9-resetxcex9(count=C)xcex9(C less than 5))xe2x86x92AX(count=C+1)]
This formula specifies that if the stall and reset signals are deasserted and the counter value is less than 5, then the counter increments by 1 in the next step. The model checker explores the entire reachable state space to verify the property. However, in reality, it ascertains the correctness of the condition on count (that it increments correctly) only in those states that are immediate successors of states satisfying the antecedent. The actual checking of the correctness condition on the model state space is thus constrained by the CTL formula. Thus, this property cannot be said to provide 100% coverage. This example illustrates the need to define a coverage measure for formally verified properties.
For this and other reasons, there is a need for the present invention.
One aspect of the present invention is a method of measuring coverage of a formal verification property. The method includes receiving a model of a logic design wherein the model has a plurality of states. The method also includes receiving a property verified for the model of the logic design and receiving one or more observed signals for the property. The method further includes providing a set of covered states in which checking a value of the one or more observed signals is sufficient to determine the validity of the verified property.
A further aspect of the present invention is an alternate method of measuring coverage of a formal verification property. The method includes receiving a model of a logic design wherein the model has a plurality of states. The method also includes receiving a property verified for the model of the logic design and receiving one or more observed signals for the property. The method further includes providing a set of covered states for the observed signal of the property, wherein the set of covered states comprise each one of the states in which changing a value of the observed signal in the state causes the property to fail.